g:IMonoid, e:|g|, a, b:. a+b x(*;e) e = (a x(*;e) e * b x(*;e) e)  |g| 

latex

Up	groups 1
Definitions	, |g|, x:A. B(x), x:AB(x), GrpSig, {x:A| B(x)} , t  T, IMonoid, n x(op;id) e, P  Q, P & Q, x:A  B(x), s = t, P  Q, P  Q, , x.A(x), n+m, x f y, f(a), (op,id) lb  i < ub. E(i), x. t(x), {i..j}, #$n, e, *, -n, Type, T, A  B, A, False, True
Lemmas	true wf, squash wf, itop shift, grp op wf, grp id wf, int seg wf, itop wf, itop split, imon wf, grp car wf, nat wf